WORST_CASE(?,O(n^3)) * Step 1: DependencyPairs WORST_CASE(?,O(n^3)) + Considered Problem: - Strict TRS: choice(dd(x,xs)) -> x choice(dd(x,xs)) -> choice(xs) eq(#1(x),#1(y)) -> eq(x,y) eq(#1(x),O(y)) -> false() eq(O(x),#1(y)) -> false() eq(O(x),O(y)) -> eq(x,y) eq(nil(),nil()) -> true() guess(dd(clause,cnf)) -> dd(choice(clause),guess(cnf)) guess(nil()) -> nil() if(false(),t,e) -> e if(true(),t,e) -> t member(x,dd(y,ys)) -> if(eq(x,y),true(),member(x,ys)) member(x,nil()) -> false() negate(#0(x)) -> #1(x) negate(#1(x)) -> #0(x) sat(cnf) -> satck(cnf,guess(cnf)) satck(cnf,assign) -> if(verify(assign),assign,unsat()) verify(dd(l,ls)) -> if(member(negate(l),ls),false(),verify(ls)) verify(nil()) -> true() - Signature: {choice/1,eq/2,guess/1,if/3,member/2,negate/1,sat/1,satck/2,verify/1} / {#0/1,#1/1,O/1,dd/2,false/0,nil/0 ,true/0,unsat/0} - Obligation: innermost runtime complexity wrt. defined symbols {choice,eq,guess,if,member,negate,sat,satck ,verify} and constructors {#0,#1,O,dd,false,nil,true,unsat} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs choice#(dd(x,xs)) -> c_1() choice#(dd(x,xs)) -> c_2(choice#(xs)) eq#(#1(x),#1(y)) -> c_3(eq#(x,y)) eq#(#1(x),O(y)) -> c_4() eq#(O(x),#1(y)) -> c_5() eq#(O(x),O(y)) -> c_6(eq#(x,y)) eq#(nil(),nil()) -> c_7() guess#(dd(clause,cnf)) -> c_8(choice#(clause),guess#(cnf)) guess#(nil()) -> c_9() if#(false(),t,e) -> c_10() if#(true(),t,e) -> c_11() member#(x,dd(y,ys)) -> c_12(if#(eq(x,y),true(),member(x,ys)),eq#(x,y),member#(x,ys)) member#(x,nil()) -> c_13() negate#(#0(x)) -> c_14() negate#(#1(x)) -> c_15() sat#(cnf) -> c_16(satck#(cnf,guess(cnf)),guess#(cnf)) satck#(cnf,assign) -> c_17(if#(verify(assign),assign,unsat()),verify#(assign)) verify#(dd(l,ls)) -> c_18(if#(member(negate(l),ls),false(),verify(ls)) ,member#(negate(l),ls) ,negate#(l) ,verify#(ls)) verify#(nil()) -> c_19() Weak DPs and mark the set of starting terms. * Step 2: PredecessorEstimation WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: choice#(dd(x,xs)) -> c_1() choice#(dd(x,xs)) -> c_2(choice#(xs)) eq#(#1(x),#1(y)) -> c_3(eq#(x,y)) eq#(#1(x),O(y)) -> c_4() eq#(O(x),#1(y)) -> c_5() eq#(O(x),O(y)) -> c_6(eq#(x,y)) eq#(nil(),nil()) -> c_7() guess#(dd(clause,cnf)) -> c_8(choice#(clause),guess#(cnf)) guess#(nil()) -> c_9() if#(false(),t,e) -> c_10() if#(true(),t,e) -> c_11() member#(x,dd(y,ys)) -> c_12(if#(eq(x,y),true(),member(x,ys)),eq#(x,y),member#(x,ys)) member#(x,nil()) -> c_13() negate#(#0(x)) -> c_14() negate#(#1(x)) -> c_15() sat#(cnf) -> c_16(satck#(cnf,guess(cnf)),guess#(cnf)) satck#(cnf,assign) -> c_17(if#(verify(assign),assign,unsat()),verify#(assign)) verify#(dd(l,ls)) -> c_18(if#(member(negate(l),ls),false(),verify(ls)) ,member#(negate(l),ls) ,negate#(l) ,verify#(ls)) verify#(nil()) -> c_19() - Weak TRS: choice(dd(x,xs)) -> x choice(dd(x,xs)) -> choice(xs) eq(#1(x),#1(y)) -> eq(x,y) eq(#1(x),O(y)) -> false() eq(O(x),#1(y)) -> false() eq(O(x),O(y)) -> eq(x,y) eq(nil(),nil()) -> true() guess(dd(clause,cnf)) -> dd(choice(clause),guess(cnf)) guess(nil()) -> nil() if(false(),t,e) -> e if(true(),t,e) -> t member(x,dd(y,ys)) -> if(eq(x,y),true(),member(x,ys)) member(x,nil()) -> false() negate(#0(x)) -> #1(x) negate(#1(x)) -> #0(x) sat(cnf) -> satck(cnf,guess(cnf)) satck(cnf,assign) -> if(verify(assign),assign,unsat()) verify(dd(l,ls)) -> if(member(negate(l),ls),false(),verify(ls)) verify(nil()) -> true() - Signature: {choice/1,eq/2,guess/1,if/3,member/2,negate/1,sat/1,satck/2,verify/1,choice#/1,eq#/2,guess#/1,if#/3 ,member#/2,negate#/1,sat#/1,satck#/2,verify#/1} / {#0/1,#1/1,O/1,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0 ,c_2/1,c_3/1,c_4/0,c_5/0,c_6/1,c_7/0,c_8/2,c_9/0,c_10/0,c_11/0,c_12/3,c_13/0,c_14/0,c_15/0,c_16/2,c_17/2 ,c_18/4,c_19/0} - Obligation: innermost runtime complexity wrt. defined symbols {choice#,eq#,guess#,if#,member#,negate#,sat#,satck# ,verify#} and constructors {#0,#1,O,dd,false,nil,true,unsat} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,4,5,7,9,10,11,13,14,15,19} by application of Pre({1,4,5,7,9,10,11,13,14,15,19}) = {2,3,6,8,12,16,17,18}. Here rules are labelled as follows: 1: choice#(dd(x,xs)) -> c_1() 2: choice#(dd(x,xs)) -> c_2(choice#(xs)) 3: eq#(#1(x),#1(y)) -> c_3(eq#(x,y)) 4: eq#(#1(x),O(y)) -> c_4() 5: eq#(O(x),#1(y)) -> c_5() 6: eq#(O(x),O(y)) -> c_6(eq#(x,y)) 7: eq#(nil(),nil()) -> c_7() 8: guess#(dd(clause,cnf)) -> c_8(choice#(clause),guess#(cnf)) 9: guess#(nil()) -> c_9() 10: if#(false(),t,e) -> c_10() 11: if#(true(),t,e) -> c_11() 12: member#(x,dd(y,ys)) -> c_12(if#(eq(x,y),true(),member(x,ys)),eq#(x,y),member#(x,ys)) 13: member#(x,nil()) -> c_13() 14: negate#(#0(x)) -> c_14() 15: negate#(#1(x)) -> c_15() 16: sat#(cnf) -> c_16(satck#(cnf,guess(cnf)),guess#(cnf)) 17: satck#(cnf,assign) -> c_17(if#(verify(assign),assign,unsat()),verify#(assign)) 18: verify#(dd(l,ls)) -> c_18(if#(member(negate(l),ls),false(),verify(ls)) ,member#(negate(l),ls) ,negate#(l) ,verify#(ls)) 19: verify#(nil()) -> c_19() * Step 3: RemoveWeakSuffixes WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: choice#(dd(x,xs)) -> c_2(choice#(xs)) eq#(#1(x),#1(y)) -> c_3(eq#(x,y)) eq#(O(x),O(y)) -> c_6(eq#(x,y)) guess#(dd(clause,cnf)) -> c_8(choice#(clause),guess#(cnf)) member#(x,dd(y,ys)) -> c_12(if#(eq(x,y),true(),member(x,ys)),eq#(x,y),member#(x,ys)) sat#(cnf) -> c_16(satck#(cnf,guess(cnf)),guess#(cnf)) satck#(cnf,assign) -> c_17(if#(verify(assign),assign,unsat()),verify#(assign)) verify#(dd(l,ls)) -> c_18(if#(member(negate(l),ls),false(),verify(ls)) ,member#(negate(l),ls) ,negate#(l) ,verify#(ls)) - Weak DPs: choice#(dd(x,xs)) -> c_1() eq#(#1(x),O(y)) -> c_4() eq#(O(x),#1(y)) -> c_5() eq#(nil(),nil()) -> c_7() guess#(nil()) -> c_9() if#(false(),t,e) -> c_10() if#(true(),t,e) -> c_11() member#(x,nil()) -> c_13() negate#(#0(x)) -> c_14() negate#(#1(x)) -> c_15() verify#(nil()) -> c_19() - Weak TRS: choice(dd(x,xs)) -> x choice(dd(x,xs)) -> choice(xs) eq(#1(x),#1(y)) -> eq(x,y) eq(#1(x),O(y)) -> false() eq(O(x),#1(y)) -> false() eq(O(x),O(y)) -> eq(x,y) eq(nil(),nil()) -> true() guess(dd(clause,cnf)) -> dd(choice(clause),guess(cnf)) guess(nil()) -> nil() if(false(),t,e) -> e if(true(),t,e) -> t member(x,dd(y,ys)) -> if(eq(x,y),true(),member(x,ys)) member(x,nil()) -> false() negate(#0(x)) -> #1(x) negate(#1(x)) -> #0(x) sat(cnf) -> satck(cnf,guess(cnf)) satck(cnf,assign) -> if(verify(assign),assign,unsat()) verify(dd(l,ls)) -> if(member(negate(l),ls),false(),verify(ls)) verify(nil()) -> true() - Signature: {choice/1,eq/2,guess/1,if/3,member/2,negate/1,sat/1,satck/2,verify/1,choice#/1,eq#/2,guess#/1,if#/3 ,member#/2,negate#/1,sat#/1,satck#/2,verify#/1} / {#0/1,#1/1,O/1,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0 ,c_2/1,c_3/1,c_4/0,c_5/0,c_6/1,c_7/0,c_8/2,c_9/0,c_10/0,c_11/0,c_12/3,c_13/0,c_14/0,c_15/0,c_16/2,c_17/2 ,c_18/4,c_19/0} - Obligation: innermost runtime complexity wrt. defined symbols {choice#,eq#,guess#,if#,member#,negate#,sat#,satck# ,verify#} and constructors {#0,#1,O,dd,false,nil,true,unsat} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:choice#(dd(x,xs)) -> c_2(choice#(xs)) -->_1 choice#(dd(x,xs)) -> c_1():9 -->_1 choice#(dd(x,xs)) -> c_2(choice#(xs)):1 2:S:eq#(#1(x),#1(y)) -> c_3(eq#(x,y)) -->_1 eq#(O(x),O(y)) -> c_6(eq#(x,y)):3 -->_1 eq#(nil(),nil()) -> c_7():12 -->_1 eq#(O(x),#1(y)) -> c_5():11 -->_1 eq#(#1(x),O(y)) -> c_4():10 -->_1 eq#(#1(x),#1(y)) -> c_3(eq#(x,y)):2 3:S:eq#(O(x),O(y)) -> c_6(eq#(x,y)) -->_1 eq#(nil(),nil()) -> c_7():12 -->_1 eq#(O(x),#1(y)) -> c_5():11 -->_1 eq#(#1(x),O(y)) -> c_4():10 -->_1 eq#(O(x),O(y)) -> c_6(eq#(x,y)):3 -->_1 eq#(#1(x),#1(y)) -> c_3(eq#(x,y)):2 4:S:guess#(dd(clause,cnf)) -> c_8(choice#(clause),guess#(cnf)) -->_2 guess#(nil()) -> c_9():13 -->_1 choice#(dd(x,xs)) -> c_1():9 -->_2 guess#(dd(clause,cnf)) -> c_8(choice#(clause),guess#(cnf)):4 -->_1 choice#(dd(x,xs)) -> c_2(choice#(xs)):1 5:S:member#(x,dd(y,ys)) -> c_12(if#(eq(x,y),true(),member(x,ys)),eq#(x,y),member#(x,ys)) -->_3 member#(x,nil()) -> c_13():16 -->_1 if#(true(),t,e) -> c_11():15 -->_1 if#(false(),t,e) -> c_10():14 -->_2 eq#(nil(),nil()) -> c_7():12 -->_2 eq#(O(x),#1(y)) -> c_5():11 -->_2 eq#(#1(x),O(y)) -> c_4():10 -->_3 member#(x,dd(y,ys)) -> c_12(if#(eq(x,y),true(),member(x,ys)),eq#(x,y),member#(x,ys)):5 -->_2 eq#(O(x),O(y)) -> c_6(eq#(x,y)):3 -->_2 eq#(#1(x),#1(y)) -> c_3(eq#(x,y)):2 6:S:sat#(cnf) -> c_16(satck#(cnf,guess(cnf)),guess#(cnf)) -->_1 satck#(cnf,assign) -> c_17(if#(verify(assign),assign,unsat()),verify#(assign)):7 -->_2 guess#(nil()) -> c_9():13 -->_2 guess#(dd(clause,cnf)) -> c_8(choice#(clause),guess#(cnf)):4 7:S:satck#(cnf,assign) -> c_17(if#(verify(assign),assign,unsat()),verify#(assign)) -->_2 verify#(dd(l,ls)) -> c_18(if#(member(negate(l),ls),false(),verify(ls)) ,member#(negate(l),ls) ,negate#(l) ,verify#(ls)):8 -->_2 verify#(nil()) -> c_19():19 -->_1 if#(true(),t,e) -> c_11():15 -->_1 if#(false(),t,e) -> c_10():14 8:S:verify#(dd(l,ls)) -> c_18(if#(member(negate(l),ls),false(),verify(ls)) ,member#(negate(l),ls) ,negate#(l) ,verify#(ls)) -->_4 verify#(nil()) -> c_19():19 -->_3 negate#(#1(x)) -> c_15():18 -->_3 negate#(#0(x)) -> c_14():17 -->_2 member#(x,nil()) -> c_13():16 -->_1 if#(true(),t,e) -> c_11():15 -->_1 if#(false(),t,e) -> c_10():14 -->_4 verify#(dd(l,ls)) -> c_18(if#(member(negate(l),ls),false(),verify(ls)) ,member#(negate(l),ls) ,negate#(l) ,verify#(ls)):8 -->_2 member#(x,dd(y,ys)) -> c_12(if#(eq(x,y),true(),member(x,ys)),eq#(x,y),member#(x,ys)):5 9:W:choice#(dd(x,xs)) -> c_1() 10:W:eq#(#1(x),O(y)) -> c_4() 11:W:eq#(O(x),#1(y)) -> c_5() 12:W:eq#(nil(),nil()) -> c_7() 13:W:guess#(nil()) -> c_9() 14:W:if#(false(),t,e) -> c_10() 15:W:if#(true(),t,e) -> c_11() 16:W:member#(x,nil()) -> c_13() 17:W:negate#(#0(x)) -> c_14() 18:W:negate#(#1(x)) -> c_15() 19:W:verify#(nil()) -> c_19() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 17: negate#(#0(x)) -> c_14() 18: negate#(#1(x)) -> c_15() 19: verify#(nil()) -> c_19() 14: if#(false(),t,e) -> c_10() 15: if#(true(),t,e) -> c_11() 16: member#(x,nil()) -> c_13() 13: guess#(nil()) -> c_9() 10: eq#(#1(x),O(y)) -> c_4() 11: eq#(O(x),#1(y)) -> c_5() 12: eq#(nil(),nil()) -> c_7() 9: choice#(dd(x,xs)) -> c_1() * Step 4: SimplifyRHS WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: choice#(dd(x,xs)) -> c_2(choice#(xs)) eq#(#1(x),#1(y)) -> c_3(eq#(x,y)) eq#(O(x),O(y)) -> c_6(eq#(x,y)) guess#(dd(clause,cnf)) -> c_8(choice#(clause),guess#(cnf)) member#(x,dd(y,ys)) -> c_12(if#(eq(x,y),true(),member(x,ys)),eq#(x,y),member#(x,ys)) sat#(cnf) -> c_16(satck#(cnf,guess(cnf)),guess#(cnf)) satck#(cnf,assign) -> c_17(if#(verify(assign),assign,unsat()),verify#(assign)) verify#(dd(l,ls)) -> c_18(if#(member(negate(l),ls),false(),verify(ls)) ,member#(negate(l),ls) ,negate#(l) ,verify#(ls)) - Weak TRS: choice(dd(x,xs)) -> x choice(dd(x,xs)) -> choice(xs) eq(#1(x),#1(y)) -> eq(x,y) eq(#1(x),O(y)) -> false() eq(O(x),#1(y)) -> false() eq(O(x),O(y)) -> eq(x,y) eq(nil(),nil()) -> true() guess(dd(clause,cnf)) -> dd(choice(clause),guess(cnf)) guess(nil()) -> nil() if(false(),t,e) -> e if(true(),t,e) -> t member(x,dd(y,ys)) -> if(eq(x,y),true(),member(x,ys)) member(x,nil()) -> false() negate(#0(x)) -> #1(x) negate(#1(x)) -> #0(x) sat(cnf) -> satck(cnf,guess(cnf)) satck(cnf,assign) -> if(verify(assign),assign,unsat()) verify(dd(l,ls)) -> if(member(negate(l),ls),false(),verify(ls)) verify(nil()) -> true() - Signature: {choice/1,eq/2,guess/1,if/3,member/2,negate/1,sat/1,satck/2,verify/1,choice#/1,eq#/2,guess#/1,if#/3 ,member#/2,negate#/1,sat#/1,satck#/2,verify#/1} / {#0/1,#1/1,O/1,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0 ,c_2/1,c_3/1,c_4/0,c_5/0,c_6/1,c_7/0,c_8/2,c_9/0,c_10/0,c_11/0,c_12/3,c_13/0,c_14/0,c_15/0,c_16/2,c_17/2 ,c_18/4,c_19/0} - Obligation: innermost runtime complexity wrt. defined symbols {choice#,eq#,guess#,if#,member#,negate#,sat#,satck# ,verify#} and constructors {#0,#1,O,dd,false,nil,true,unsat} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:choice#(dd(x,xs)) -> c_2(choice#(xs)) -->_1 choice#(dd(x,xs)) -> c_2(choice#(xs)):1 2:S:eq#(#1(x),#1(y)) -> c_3(eq#(x,y)) -->_1 eq#(O(x),O(y)) -> c_6(eq#(x,y)):3 -->_1 eq#(#1(x),#1(y)) -> c_3(eq#(x,y)):2 3:S:eq#(O(x),O(y)) -> c_6(eq#(x,y)) -->_1 eq#(O(x),O(y)) -> c_6(eq#(x,y)):3 -->_1 eq#(#1(x),#1(y)) -> c_3(eq#(x,y)):2 4:S:guess#(dd(clause,cnf)) -> c_8(choice#(clause),guess#(cnf)) -->_2 guess#(dd(clause,cnf)) -> c_8(choice#(clause),guess#(cnf)):4 -->_1 choice#(dd(x,xs)) -> c_2(choice#(xs)):1 5:S:member#(x,dd(y,ys)) -> c_12(if#(eq(x,y),true(),member(x,ys)),eq#(x,y),member#(x,ys)) -->_3 member#(x,dd(y,ys)) -> c_12(if#(eq(x,y),true(),member(x,ys)),eq#(x,y),member#(x,ys)):5 -->_2 eq#(O(x),O(y)) -> c_6(eq#(x,y)):3 -->_2 eq#(#1(x),#1(y)) -> c_3(eq#(x,y)):2 6:S:sat#(cnf) -> c_16(satck#(cnf,guess(cnf)),guess#(cnf)) -->_1 satck#(cnf,assign) -> c_17(if#(verify(assign),assign,unsat()),verify#(assign)):7 -->_2 guess#(dd(clause,cnf)) -> c_8(choice#(clause),guess#(cnf)):4 7:S:satck#(cnf,assign) -> c_17(if#(verify(assign),assign,unsat()),verify#(assign)) -->_2 verify#(dd(l,ls)) -> c_18(if#(member(negate(l),ls),false(),verify(ls)) ,member#(negate(l),ls) ,negate#(l) ,verify#(ls)):8 8:S:verify#(dd(l,ls)) -> c_18(if#(member(negate(l),ls),false(),verify(ls)) ,member#(negate(l),ls) ,negate#(l) ,verify#(ls)) -->_4 verify#(dd(l,ls)) -> c_18(if#(member(negate(l),ls),false(),verify(ls)) ,member#(negate(l),ls) ,negate#(l) ,verify#(ls)):8 -->_2 member#(x,dd(y,ys)) -> c_12(if#(eq(x,y),true(),member(x,ys)),eq#(x,y),member#(x,ys)):5 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: member#(x,dd(y,ys)) -> c_12(eq#(x,y),member#(x,ys)) satck#(cnf,assign) -> c_17(verify#(assign)) verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls)) * Step 5: UsableRules WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: choice#(dd(x,xs)) -> c_2(choice#(xs)) eq#(#1(x),#1(y)) -> c_3(eq#(x,y)) eq#(O(x),O(y)) -> c_6(eq#(x,y)) guess#(dd(clause,cnf)) -> c_8(choice#(clause),guess#(cnf)) member#(x,dd(y,ys)) -> c_12(eq#(x,y),member#(x,ys)) sat#(cnf) -> c_16(satck#(cnf,guess(cnf)),guess#(cnf)) satck#(cnf,assign) -> c_17(verify#(assign)) verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls)) - Weak TRS: choice(dd(x,xs)) -> x choice(dd(x,xs)) -> choice(xs) eq(#1(x),#1(y)) -> eq(x,y) eq(#1(x),O(y)) -> false() eq(O(x),#1(y)) -> false() eq(O(x),O(y)) -> eq(x,y) eq(nil(),nil()) -> true() guess(dd(clause,cnf)) -> dd(choice(clause),guess(cnf)) guess(nil()) -> nil() if(false(),t,e) -> e if(true(),t,e) -> t member(x,dd(y,ys)) -> if(eq(x,y),true(),member(x,ys)) member(x,nil()) -> false() negate(#0(x)) -> #1(x) negate(#1(x)) -> #0(x) sat(cnf) -> satck(cnf,guess(cnf)) satck(cnf,assign) -> if(verify(assign),assign,unsat()) verify(dd(l,ls)) -> if(member(negate(l),ls),false(),verify(ls)) verify(nil()) -> true() - Signature: {choice/1,eq/2,guess/1,if/3,member/2,negate/1,sat/1,satck/2,verify/1,choice#/1,eq#/2,guess#/1,if#/3 ,member#/2,negate#/1,sat#/1,satck#/2,verify#/1} / {#0/1,#1/1,O/1,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0 ,c_2/1,c_3/1,c_4/0,c_5/0,c_6/1,c_7/0,c_8/2,c_9/0,c_10/0,c_11/0,c_12/2,c_13/0,c_14/0,c_15/0,c_16/2,c_17/1 ,c_18/2,c_19/0} - Obligation: innermost runtime complexity wrt. defined symbols {choice#,eq#,guess#,if#,member#,negate#,sat#,satck# ,verify#} and constructors {#0,#1,O,dd,false,nil,true,unsat} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: choice(dd(x,xs)) -> x choice(dd(x,xs)) -> choice(xs) guess(dd(clause,cnf)) -> dd(choice(clause),guess(cnf)) guess(nil()) -> nil() negate(#0(x)) -> #1(x) negate(#1(x)) -> #0(x) choice#(dd(x,xs)) -> c_2(choice#(xs)) eq#(#1(x),#1(y)) -> c_3(eq#(x,y)) eq#(O(x),O(y)) -> c_6(eq#(x,y)) guess#(dd(clause,cnf)) -> c_8(choice#(clause),guess#(cnf)) member#(x,dd(y,ys)) -> c_12(eq#(x,y),member#(x,ys)) sat#(cnf) -> c_16(satck#(cnf,guess(cnf)),guess#(cnf)) satck#(cnf,assign) -> c_17(verify#(assign)) verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls)) * Step 6: DecomposeDG WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: choice#(dd(x,xs)) -> c_2(choice#(xs)) eq#(#1(x),#1(y)) -> c_3(eq#(x,y)) eq#(O(x),O(y)) -> c_6(eq#(x,y)) guess#(dd(clause,cnf)) -> c_8(choice#(clause),guess#(cnf)) member#(x,dd(y,ys)) -> c_12(eq#(x,y),member#(x,ys)) sat#(cnf) -> c_16(satck#(cnf,guess(cnf)),guess#(cnf)) satck#(cnf,assign) -> c_17(verify#(assign)) verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls)) - Weak TRS: choice(dd(x,xs)) -> x choice(dd(x,xs)) -> choice(xs) guess(dd(clause,cnf)) -> dd(choice(clause),guess(cnf)) guess(nil()) -> nil() negate(#0(x)) -> #1(x) negate(#1(x)) -> #0(x) - Signature: {choice/1,eq/2,guess/1,if/3,member/2,negate/1,sat/1,satck/2,verify/1,choice#/1,eq#/2,guess#/1,if#/3 ,member#/2,negate#/1,sat#/1,satck#/2,verify#/1} / {#0/1,#1/1,O/1,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0 ,c_2/1,c_3/1,c_4/0,c_5/0,c_6/1,c_7/0,c_8/2,c_9/0,c_10/0,c_11/0,c_12/2,c_13/0,c_14/0,c_15/0,c_16/2,c_17/1 ,c_18/2,c_19/0} - Obligation: innermost runtime complexity wrt. defined symbols {choice#,eq#,guess#,if#,member#,negate#,sat#,satck# ,verify#} and constructors {#0,#1,O,dd,false,nil,true,unsat} + Applied Processor: DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing} + Details: We decompose the input problem according to the dependency graph into the upper component guess#(dd(clause,cnf)) -> c_8(choice#(clause),guess#(cnf)) sat#(cnf) -> c_16(satck#(cnf,guess(cnf)),guess#(cnf)) satck#(cnf,assign) -> c_17(verify#(assign)) verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls)) and a lower component choice#(dd(x,xs)) -> c_2(choice#(xs)) eq#(#1(x),#1(y)) -> c_3(eq#(x,y)) eq#(O(x),O(y)) -> c_6(eq#(x,y)) member#(x,dd(y,ys)) -> c_12(eq#(x,y),member#(x,ys)) Further, following extension rules are added to the lower component. guess#(dd(clause,cnf)) -> choice#(clause) guess#(dd(clause,cnf)) -> guess#(cnf) sat#(cnf) -> guess#(cnf) sat#(cnf) -> satck#(cnf,guess(cnf)) satck#(cnf,assign) -> verify#(assign) verify#(dd(l,ls)) -> member#(negate(l),ls) verify#(dd(l,ls)) -> verify#(ls) ** Step 6.a:1: SimplifyRHS WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: guess#(dd(clause,cnf)) -> c_8(choice#(clause),guess#(cnf)) sat#(cnf) -> c_16(satck#(cnf,guess(cnf)),guess#(cnf)) satck#(cnf,assign) -> c_17(verify#(assign)) verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls)) - Weak TRS: choice(dd(x,xs)) -> x choice(dd(x,xs)) -> choice(xs) guess(dd(clause,cnf)) -> dd(choice(clause),guess(cnf)) guess(nil()) -> nil() negate(#0(x)) -> #1(x) negate(#1(x)) -> #0(x) - Signature: {choice/1,eq/2,guess/1,if/3,member/2,negate/1,sat/1,satck/2,verify/1,choice#/1,eq#/2,guess#/1,if#/3 ,member#/2,negate#/1,sat#/1,satck#/2,verify#/1} / {#0/1,#1/1,O/1,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0 ,c_2/1,c_3/1,c_4/0,c_5/0,c_6/1,c_7/0,c_8/2,c_9/0,c_10/0,c_11/0,c_12/2,c_13/0,c_14/0,c_15/0,c_16/2,c_17/1 ,c_18/2,c_19/0} - Obligation: innermost runtime complexity wrt. defined symbols {choice#,eq#,guess#,if#,member#,negate#,sat#,satck# ,verify#} and constructors {#0,#1,O,dd,false,nil,true,unsat} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:guess#(dd(clause,cnf)) -> c_8(choice#(clause),guess#(cnf)) -->_2 guess#(dd(clause,cnf)) -> c_8(choice#(clause),guess#(cnf)):1 2:S:sat#(cnf) -> c_16(satck#(cnf,guess(cnf)),guess#(cnf)) -->_1 satck#(cnf,assign) -> c_17(verify#(assign)):3 -->_2 guess#(dd(clause,cnf)) -> c_8(choice#(clause),guess#(cnf)):1 3:S:satck#(cnf,assign) -> c_17(verify#(assign)) -->_1 verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls)):4 4:S:verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls)) -->_2 verify#(dd(l,ls)) -> c_18(member#(negate(l),ls),verify#(ls)):4 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: guess#(dd(clause,cnf)) -> c_8(guess#(cnf)) verify#(dd(l,ls)) -> c_18(verify#(ls)) ** Step 6.a:2: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: guess#(dd(clause,cnf)) -> c_8(guess#(cnf)) sat#(cnf) -> c_16(satck#(cnf,guess(cnf)),guess#(cnf)) satck#(cnf,assign) -> c_17(verify#(assign)) verify#(dd(l,ls)) -> c_18(verify#(ls)) - Weak TRS: choice(dd(x,xs)) -> x choice(dd(x,xs)) -> choice(xs) guess(dd(clause,cnf)) -> dd(choice(clause),guess(cnf)) guess(nil()) -> nil() negate(#0(x)) -> #1(x) negate(#1(x)) -> #0(x) - Signature: {choice/1,eq/2,guess/1,if/3,member/2,negate/1,sat/1,satck/2,verify/1,choice#/1,eq#/2,guess#/1,if#/3 ,member#/2,negate#/1,sat#/1,satck#/2,verify#/1} / {#0/1,#1/1,O/1,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0 ,c_2/1,c_3/1,c_4/0,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0,c_10/0,c_11/0,c_12/2,c_13/0,c_14/0,c_15/0,c_16/2,c_17/1 ,c_18/1,c_19/0} - Obligation: innermost runtime complexity wrt. defined symbols {choice#,eq#,guess#,if#,member#,negate#,sat#,satck# ,verify#} and constructors {#0,#1,O,dd,false,nil,true,unsat} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: choice(dd(x,xs)) -> x choice(dd(x,xs)) -> choice(xs) guess(dd(clause,cnf)) -> dd(choice(clause),guess(cnf)) guess(nil()) -> nil() guess#(dd(clause,cnf)) -> c_8(guess#(cnf)) sat#(cnf) -> c_16(satck#(cnf,guess(cnf)),guess#(cnf)) satck#(cnf,assign) -> c_17(verify#(assign)) verify#(dd(l,ls)) -> c_18(verify#(ls)) ** Step 6.a:3: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: guess#(dd(clause,cnf)) -> c_8(guess#(cnf)) sat#(cnf) -> c_16(satck#(cnf,guess(cnf)),guess#(cnf)) satck#(cnf,assign) -> c_17(verify#(assign)) verify#(dd(l,ls)) -> c_18(verify#(ls)) - Weak TRS: choice(dd(x,xs)) -> x choice(dd(x,xs)) -> choice(xs) guess(dd(clause,cnf)) -> dd(choice(clause),guess(cnf)) guess(nil()) -> nil() - Signature: {choice/1,eq/2,guess/1,if/3,member/2,negate/1,sat/1,satck/2,verify/1,choice#/1,eq#/2,guess#/1,if#/3 ,member#/2,negate#/1,sat#/1,satck#/2,verify#/1} / {#0/1,#1/1,O/1,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0 ,c_2/1,c_3/1,c_4/0,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0,c_10/0,c_11/0,c_12/2,c_13/0,c_14/0,c_15/0,c_16/2,c_17/1 ,c_18/1,c_19/0} - Obligation: innermost runtime complexity wrt. defined symbols {choice#,eq#,guess#,if#,member#,negate#,sat#,satck# ,verify#} and constructors {#0,#1,O,dd,false,nil,true,unsat} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- choice :: ["A"(0)] -(0)-> "A"(0) dd :: ["A"(0) x "A"(0)] -(0)-> "A"(0) guess :: ["A"(0)] -(0)-> "A"(0) nil :: [] -(0)-> "A"(0) guess# :: ["A"(0)] -(0)-> "A"(0) sat# :: ["A"(0)] -(2)-> "A"(0) satck# :: ["A"(0) x "A"(0)] -(1)-> "A"(0) verify# :: ["A"(0)] -(0)-> "A"(0) c_8 :: ["A"(0)] -(0)-> "A"(0) c_16 :: ["A"(0) x "A"(0)] -(0)-> "A"(0) c_17 :: ["A"(0)] -(0)-> "A"(0) c_18 :: ["A"(0)] -(0)-> "A"(0) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: sat#(cnf) -> c_16(satck#(cnf,guess(cnf)),guess#(cnf)) satck#(cnf,assign) -> c_17(verify#(assign)) 2. Weak: guess#(dd(clause,cnf)) -> c_8(guess#(cnf)) verify#(dd(l,ls)) -> c_18(verify#(ls)) ** Step 6.a:4: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: guess#(dd(clause,cnf)) -> c_8(guess#(cnf)) verify#(dd(l,ls)) -> c_18(verify#(ls)) - Weak DPs: sat#(cnf) -> c_16(satck#(cnf,guess(cnf)),guess#(cnf)) satck#(cnf,assign) -> c_17(verify#(assign)) - Weak TRS: choice(dd(x,xs)) -> x choice(dd(x,xs)) -> choice(xs) guess(dd(clause,cnf)) -> dd(choice(clause),guess(cnf)) guess(nil()) -> nil() - Signature: {choice/1,eq/2,guess/1,if/3,member/2,negate/1,sat/1,satck/2,verify/1,choice#/1,eq#/2,guess#/1,if#/3 ,member#/2,negate#/1,sat#/1,satck#/2,verify#/1} / {#0/1,#1/1,O/1,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0 ,c_2/1,c_3/1,c_4/0,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0,c_10/0,c_11/0,c_12/2,c_13/0,c_14/0,c_15/0,c_16/2,c_17/1 ,c_18/1,c_19/0} - Obligation: innermost runtime complexity wrt. defined symbols {choice#,eq#,guess#,if#,member#,negate#,sat#,satck# ,verify#} and constructors {#0,#1,O,dd,false,nil,true,unsat} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- choice :: ["A"(0)] -(0)-> "A"(0) dd :: ["A"(0) x "A"(8)] -(8)-> "A"(8) dd :: ["A"(0) x "A"(2)] -(2)-> "A"(2) dd :: ["A"(0) x "A"(0)] -(0)-> "A"(0) dd :: ["A"(0) x "A"(7)] -(7)-> "A"(7) guess :: ["A"(7)] -(1)-> "A"(2) nil :: [] -(0)-> "A"(7) nil :: [] -(0)-> "A"(14) guess# :: ["A"(8)] -(5)-> "A"(0) sat# :: ["A"(15)] -(15)-> "A"(0) satck# :: ["A"(0) x "A"(2)] -(7)-> "A"(8) verify# :: ["A"(2)] -(7)-> "A"(0) c_8 :: ["A"(0)] -(0)-> "A"(0) c_16 :: ["A"(0) x "A"(0)] -(0)-> "A"(0) c_17 :: ["A"(0)] -(0)-> "A"(8) c_18 :: ["A"(0)] -(0)-> "A"(0) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "c_16_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1) "c_17_A" :: ["A"(0)] -(0)-> "A"(1) "c_18_A" :: ["A"(0)] -(1)-> "A"(1) "c_8_A" :: ["A"(0)] -(0)-> "A"(1) "dd_A" :: ["A"(0) x "A"(1)] -(1)-> "A"(1) "nil_A" :: [] -(0)-> "A"(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: guess#(dd(clause,cnf)) -> c_8(guess#(cnf)) verify#(dd(l,ls)) -> c_18(verify#(ls)) 2. Weak: ** Step 6.b:1: DecomposeDG WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: choice#(dd(x,xs)) -> c_2(choice#(xs)) eq#(#1(x),#1(y)) -> c_3(eq#(x,y)) eq#(O(x),O(y)) -> c_6(eq#(x,y)) member#(x,dd(y,ys)) -> c_12(eq#(x,y),member#(x,ys)) - Weak DPs: guess#(dd(clause,cnf)) -> choice#(clause) guess#(dd(clause,cnf)) -> guess#(cnf) sat#(cnf) -> guess#(cnf) sat#(cnf) -> satck#(cnf,guess(cnf)) satck#(cnf,assign) -> verify#(assign) verify#(dd(l,ls)) -> member#(negate(l),ls) verify#(dd(l,ls)) -> verify#(ls) - Weak TRS: choice(dd(x,xs)) -> x choice(dd(x,xs)) -> choice(xs) guess(dd(clause,cnf)) -> dd(choice(clause),guess(cnf)) guess(nil()) -> nil() negate(#0(x)) -> #1(x) negate(#1(x)) -> #0(x) - Signature: {choice/1,eq/2,guess/1,if/3,member/2,negate/1,sat/1,satck/2,verify/1,choice#/1,eq#/2,guess#/1,if#/3 ,member#/2,negate#/1,sat#/1,satck#/2,verify#/1} / {#0/1,#1/1,O/1,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0 ,c_2/1,c_3/1,c_4/0,c_5/0,c_6/1,c_7/0,c_8/2,c_9/0,c_10/0,c_11/0,c_12/2,c_13/0,c_14/0,c_15/0,c_16/2,c_17/1 ,c_18/2,c_19/0} - Obligation: innermost runtime complexity wrt. defined symbols {choice#,eq#,guess#,if#,member#,negate#,sat#,satck# ,verify#} and constructors {#0,#1,O,dd,false,nil,true,unsat} + Applied Processor: DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing} + Details: We decompose the input problem according to the dependency graph into the upper component choice#(dd(x,xs)) -> c_2(choice#(xs)) guess#(dd(clause,cnf)) -> choice#(clause) guess#(dd(clause,cnf)) -> guess#(cnf) member#(x,dd(y,ys)) -> c_12(eq#(x,y),member#(x,ys)) sat#(cnf) -> guess#(cnf) sat#(cnf) -> satck#(cnf,guess(cnf)) satck#(cnf,assign) -> verify#(assign) verify#(dd(l,ls)) -> member#(negate(l),ls) verify#(dd(l,ls)) -> verify#(ls) and a lower component eq#(#1(x),#1(y)) -> c_3(eq#(x,y)) eq#(O(x),O(y)) -> c_6(eq#(x,y)) Further, following extension rules are added to the lower component. choice#(dd(x,xs)) -> choice#(xs) guess#(dd(clause,cnf)) -> choice#(clause) guess#(dd(clause,cnf)) -> guess#(cnf) member#(x,dd(y,ys)) -> eq#(x,y) member#(x,dd(y,ys)) -> member#(x,ys) sat#(cnf) -> guess#(cnf) sat#(cnf) -> satck#(cnf,guess(cnf)) satck#(cnf,assign) -> verify#(assign) verify#(dd(l,ls)) -> member#(negate(l),ls) verify#(dd(l,ls)) -> verify#(ls) *** Step 6.b:1.a:1: RemoveHeads WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: choice#(dd(x,xs)) -> c_2(choice#(xs)) member#(x,dd(y,ys)) -> c_12(eq#(x,y),member#(x,ys)) - Weak DPs: guess#(dd(clause,cnf)) -> choice#(clause) guess#(dd(clause,cnf)) -> guess#(cnf) sat#(cnf) -> guess#(cnf) sat#(cnf) -> satck#(cnf,guess(cnf)) satck#(cnf,assign) -> verify#(assign) verify#(dd(l,ls)) -> member#(negate(l),ls) verify#(dd(l,ls)) -> verify#(ls) - Weak TRS: choice(dd(x,xs)) -> x choice(dd(x,xs)) -> choice(xs) guess(dd(clause,cnf)) -> dd(choice(clause),guess(cnf)) guess(nil()) -> nil() negate(#0(x)) -> #1(x) negate(#1(x)) -> #0(x) - Signature: {choice/1,eq/2,guess/1,if/3,member/2,negate/1,sat/1,satck/2,verify/1,choice#/1,eq#/2,guess#/1,if#/3 ,member#/2,negate#/1,sat#/1,satck#/2,verify#/1} / {#0/1,#1/1,O/1,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0 ,c_2/1,c_3/1,c_4/0,c_5/0,c_6/1,c_7/0,c_8/2,c_9/0,c_10/0,c_11/0,c_12/2,c_13/0,c_14/0,c_15/0,c_16/2,c_17/1 ,c_18/2,c_19/0} - Obligation: innermost runtime complexity wrt. defined symbols {choice#,eq#,guess#,if#,member#,negate#,sat#,satck# ,verify#} and constructors {#0,#1,O,dd,false,nil,true,unsat} + Applied Processor: RemoveHeads + Details: Consider the dependency graph 1:S:choice#(dd(x,xs)) -> c_2(choice#(xs)) -->_1 choice#(dd(x,xs)) -> c_2(choice#(xs)):1 2:S:member#(x,dd(y,ys)) -> c_12(eq#(x,y),member#(x,ys)) -->_2 member#(x,dd(y,ys)) -> c_12(eq#(x,y),member#(x,ys)):2 3:W:guess#(dd(clause,cnf)) -> choice#(clause) -->_1 choice#(dd(x,xs)) -> c_2(choice#(xs)):1 4:W:guess#(dd(clause,cnf)) -> guess#(cnf) -->_1 guess#(dd(clause,cnf)) -> guess#(cnf):4 -->_1 guess#(dd(clause,cnf)) -> choice#(clause):3 5:W:sat#(cnf) -> guess#(cnf) -->_1 guess#(dd(clause,cnf)) -> guess#(cnf):4 -->_1 guess#(dd(clause,cnf)) -> choice#(clause):3 6:W:sat#(cnf) -> satck#(cnf,guess(cnf)) -->_1 satck#(cnf,assign) -> verify#(assign):7 7:W:satck#(cnf,assign) -> verify#(assign) -->_1 verify#(dd(l,ls)) -> verify#(ls):9 -->_1 verify#(dd(l,ls)) -> member#(negate(l),ls):8 8:W:verify#(dd(l,ls)) -> member#(negate(l),ls) -->_1 member#(x,dd(y,ys)) -> c_12(eq#(x,y),member#(x,ys)):2 9:W:verify#(dd(l,ls)) -> verify#(ls) -->_1 verify#(dd(l,ls)) -> verify#(ls):9 -->_1 verify#(dd(l,ls)) -> member#(negate(l),ls):8 Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts). [(5,sat#(cnf) -> guess#(cnf))] *** Step 6.b:1.a:2: SimplifyRHS WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: choice#(dd(x,xs)) -> c_2(choice#(xs)) member#(x,dd(y,ys)) -> c_12(eq#(x,y),member#(x,ys)) - Weak DPs: guess#(dd(clause,cnf)) -> choice#(clause) guess#(dd(clause,cnf)) -> guess#(cnf) sat#(cnf) -> satck#(cnf,guess(cnf)) satck#(cnf,assign) -> verify#(assign) verify#(dd(l,ls)) -> member#(negate(l),ls) verify#(dd(l,ls)) -> verify#(ls) - Weak TRS: choice(dd(x,xs)) -> x choice(dd(x,xs)) -> choice(xs) guess(dd(clause,cnf)) -> dd(choice(clause),guess(cnf)) guess(nil()) -> nil() negate(#0(x)) -> #1(x) negate(#1(x)) -> #0(x) - Signature: {choice/1,eq/2,guess/1,if/3,member/2,negate/1,sat/1,satck/2,verify/1,choice#/1,eq#/2,guess#/1,if#/3 ,member#/2,negate#/1,sat#/1,satck#/2,verify#/1} / {#0/1,#1/1,O/1,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0 ,c_2/1,c_3/1,c_4/0,c_5/0,c_6/1,c_7/0,c_8/2,c_9/0,c_10/0,c_11/0,c_12/2,c_13/0,c_14/0,c_15/0,c_16/2,c_17/1 ,c_18/2,c_19/0} - Obligation: innermost runtime complexity wrt. defined symbols {choice#,eq#,guess#,if#,member#,negate#,sat#,satck# ,verify#} and constructors {#0,#1,O,dd,false,nil,true,unsat} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:choice#(dd(x,xs)) -> c_2(choice#(xs)) -->_1 choice#(dd(x,xs)) -> c_2(choice#(xs)):1 2:S:member#(x,dd(y,ys)) -> c_12(eq#(x,y),member#(x,ys)) -->_2 member#(x,dd(y,ys)) -> c_12(eq#(x,y),member#(x,ys)):2 3:W:guess#(dd(clause,cnf)) -> choice#(clause) -->_1 choice#(dd(x,xs)) -> c_2(choice#(xs)):1 4:W:guess#(dd(clause,cnf)) -> guess#(cnf) -->_1 guess#(dd(clause,cnf)) -> guess#(cnf):4 -->_1 guess#(dd(clause,cnf)) -> choice#(clause):3 6:W:sat#(cnf) -> satck#(cnf,guess(cnf)) -->_1 satck#(cnf,assign) -> verify#(assign):7 7:W:satck#(cnf,assign) -> verify#(assign) -->_1 verify#(dd(l,ls)) -> verify#(ls):9 -->_1 verify#(dd(l,ls)) -> member#(negate(l),ls):8 8:W:verify#(dd(l,ls)) -> member#(negate(l),ls) -->_1 member#(x,dd(y,ys)) -> c_12(eq#(x,y),member#(x,ys)):2 9:W:verify#(dd(l,ls)) -> verify#(ls) -->_1 verify#(dd(l,ls)) -> verify#(ls):9 -->_1 verify#(dd(l,ls)) -> member#(negate(l),ls):8 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: member#(x,dd(y,ys)) -> c_12(member#(x,ys)) *** Step 6.b:1.a:3: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: choice#(dd(x,xs)) -> c_2(choice#(xs)) member#(x,dd(y,ys)) -> c_12(member#(x,ys)) - Weak DPs: guess#(dd(clause,cnf)) -> choice#(clause) guess#(dd(clause,cnf)) -> guess#(cnf) sat#(cnf) -> satck#(cnf,guess(cnf)) satck#(cnf,assign) -> verify#(assign) verify#(dd(l,ls)) -> member#(negate(l),ls) verify#(dd(l,ls)) -> verify#(ls) - Weak TRS: choice(dd(x,xs)) -> x choice(dd(x,xs)) -> choice(xs) guess(dd(clause,cnf)) -> dd(choice(clause),guess(cnf)) guess(nil()) -> nil() negate(#0(x)) -> #1(x) negate(#1(x)) -> #0(x) - Signature: {choice/1,eq/2,guess/1,if/3,member/2,negate/1,sat/1,satck/2,verify/1,choice#/1,eq#/2,guess#/1,if#/3 ,member#/2,negate#/1,sat#/1,satck#/2,verify#/1} / {#0/1,#1/1,O/1,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0 ,c_2/1,c_3/1,c_4/0,c_5/0,c_6/1,c_7/0,c_8/2,c_9/0,c_10/0,c_11/0,c_12/1,c_13/0,c_14/0,c_15/0,c_16/2,c_17/1 ,c_18/2,c_19/0} - Obligation: innermost runtime complexity wrt. defined symbols {choice#,eq#,guess#,if#,member#,negate#,sat#,satck# ,verify#} and constructors {#0,#1,O,dd,false,nil,true,unsat} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- #0 :: ["A"(0)] -(0)-> "A"(0) #0 :: ["A"(0)] -(0)-> "A"(14) #1 :: ["A"(0)] -(0)-> "A"(0) #1 :: ["A"(0)] -(0)-> "A"(14) choice :: ["A"(1)] -(0)-> "A"(1) dd :: ["A"(8) x "A"(8)] -(8)-> "A"(8) dd :: ["A"(1) x "A"(1)] -(1)-> "A"(1) dd :: ["A"(2) x "A"(2)] -(2)-> "A"(2) guess :: ["A"(2)] -(0)-> "A"(1) negate :: ["A"(0)] -(0)-> "A"(0) nil :: [] -(0)-> "A"(2) nil :: [] -(0)-> "A"(15) choice# :: ["A"(8)] -(0)-> "A"(0) guess# :: ["A"(8)] -(0)-> "A"(0) member# :: ["A"(0) x "A"(1)] -(15)-> "A"(0) sat# :: ["A"(14)] -(15)-> "A"(0) satck# :: ["A"(0) x "A"(1)] -(15)-> "A"(0) verify# :: ["A"(1)] -(15)-> "A"(0) c_2 :: ["A"(0)] -(0)-> "A"(10) c_12 :: ["A"(0)] -(0)-> "A"(14) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "#0_A" :: ["A"(0)] -(0)-> "A"(1) "#1_A" :: ["A"(0)] -(0)-> "A"(1) "c_12_A" :: ["A"(0)] -(0)-> "A"(1) "c_2_A" :: ["A"(0)] -(0)-> "A"(1) "dd_A" :: ["A"(1) x "A"(1)] -(1)-> "A"(1) "nil_A" :: [] -(0)-> "A"(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: choice#(dd(x,xs)) -> c_2(choice#(xs)) 2. Weak: member#(x,dd(y,ys)) -> c_12(member#(x,ys)) *** Step 6.b:1.a:4: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: member#(x,dd(y,ys)) -> c_12(member#(x,ys)) - Weak DPs: choice#(dd(x,xs)) -> c_2(choice#(xs)) guess#(dd(clause,cnf)) -> choice#(clause) guess#(dd(clause,cnf)) -> guess#(cnf) sat#(cnf) -> satck#(cnf,guess(cnf)) satck#(cnf,assign) -> verify#(assign) verify#(dd(l,ls)) -> member#(negate(l),ls) verify#(dd(l,ls)) -> verify#(ls) - Weak TRS: choice(dd(x,xs)) -> x choice(dd(x,xs)) -> choice(xs) guess(dd(clause,cnf)) -> dd(choice(clause),guess(cnf)) guess(nil()) -> nil() negate(#0(x)) -> #1(x) negate(#1(x)) -> #0(x) - Signature: {choice/1,eq/2,guess/1,if/3,member/2,negate/1,sat/1,satck/2,verify/1,choice#/1,eq#/2,guess#/1,if#/3 ,member#/2,negate#/1,sat#/1,satck#/2,verify#/1} / {#0/1,#1/1,O/1,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0 ,c_2/1,c_3/1,c_4/0,c_5/0,c_6/1,c_7/0,c_8/2,c_9/0,c_10/0,c_11/0,c_12/1,c_13/0,c_14/0,c_15/0,c_16/2,c_17/1 ,c_18/2,c_19/0} - Obligation: innermost runtime complexity wrt. defined symbols {choice#,eq#,guess#,if#,member#,negate#,sat#,satck# ,verify#} and constructors {#0,#1,O,dd,false,nil,true,unsat} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- #0 :: ["A"(0)] -(0)-> "A"(0) #0 :: ["A"(0)] -(0)-> "A"(14) #1 :: ["A"(0)] -(0)-> "A"(0) #1 :: ["A"(0)] -(0)-> "A"(14) choice :: ["A"(0)] -(0)-> "A"(0) dd :: ["A"(0) x "A"(3)] -(3)-> "A"(3) dd :: ["A"(0) x "A"(0)] -(0)-> "A"(0) guess :: ["A"(3)] -(0)-> "A"(3) negate :: ["A"(0)] -(0)-> "A"(0) nil :: [] -(0)-> "A"(3) nil :: [] -(0)-> "A"(8) choice# :: ["A"(0)] -(15)-> "A"(0) guess# :: ["A"(0)] -(15)-> "A"(0) member# :: ["A"(0) x "A"(3)] -(0)-> "A"(8) sat# :: ["A"(10)] -(14)-> "A"(0) satck# :: ["A"(0) x "A"(3)] -(8)-> "A"(0) verify# :: ["A"(3)] -(4)-> "A"(0) c_2 :: ["A"(0)] -(0)-> "A"(0) c_12 :: ["A"(0)] -(0)-> "A"(14) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "#0_A" :: ["A"(0)] -(0)-> "A"(1) "#1_A" :: ["A"(0)] -(0)-> "A"(1) "c_12_A" :: ["A"(0)] -(0)-> "A"(1) "c_2_A" :: ["A"(0)] -(0)-> "A"(1) "dd_A" :: ["A"(0) x "A"(1)] -(1)-> "A"(1) "nil_A" :: [] -(0)-> "A"(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: member#(x,dd(y,ys)) -> c_12(member#(x,ys)) 2. Weak: *** Step 6.b:1.b:1: RemoveWeakSuffixes WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: eq#(#1(x),#1(y)) -> c_3(eq#(x,y)) eq#(O(x),O(y)) -> c_6(eq#(x,y)) - Weak DPs: choice#(dd(x,xs)) -> choice#(xs) guess#(dd(clause,cnf)) -> choice#(clause) guess#(dd(clause,cnf)) -> guess#(cnf) member#(x,dd(y,ys)) -> eq#(x,y) member#(x,dd(y,ys)) -> member#(x,ys) sat#(cnf) -> guess#(cnf) sat#(cnf) -> satck#(cnf,guess(cnf)) satck#(cnf,assign) -> verify#(assign) verify#(dd(l,ls)) -> member#(negate(l),ls) verify#(dd(l,ls)) -> verify#(ls) - Weak TRS: choice(dd(x,xs)) -> x choice(dd(x,xs)) -> choice(xs) guess(dd(clause,cnf)) -> dd(choice(clause),guess(cnf)) guess(nil()) -> nil() negate(#0(x)) -> #1(x) negate(#1(x)) -> #0(x) - Signature: {choice/1,eq/2,guess/1,if/3,member/2,negate/1,sat/1,satck/2,verify/1,choice#/1,eq#/2,guess#/1,if#/3 ,member#/2,negate#/1,sat#/1,satck#/2,verify#/1} / {#0/1,#1/1,O/1,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0 ,c_2/1,c_3/1,c_4/0,c_5/0,c_6/1,c_7/0,c_8/2,c_9/0,c_10/0,c_11/0,c_12/2,c_13/0,c_14/0,c_15/0,c_16/2,c_17/1 ,c_18/2,c_19/0} - Obligation: innermost runtime complexity wrt. defined symbols {choice#,eq#,guess#,if#,member#,negate#,sat#,satck# ,verify#} and constructors {#0,#1,O,dd,false,nil,true,unsat} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:eq#(#1(x),#1(y)) -> c_3(eq#(x,y)) -->_1 eq#(O(x),O(y)) -> c_6(eq#(x,y)):2 -->_1 eq#(#1(x),#1(y)) -> c_3(eq#(x,y)):1 2:S:eq#(O(x),O(y)) -> c_6(eq#(x,y)) -->_1 eq#(O(x),O(y)) -> c_6(eq#(x,y)):2 -->_1 eq#(#1(x),#1(y)) -> c_3(eq#(x,y)):1 3:W:choice#(dd(x,xs)) -> choice#(xs) -->_1 choice#(dd(x,xs)) -> choice#(xs):3 4:W:guess#(dd(clause,cnf)) -> choice#(clause) -->_1 choice#(dd(x,xs)) -> choice#(xs):3 5:W:guess#(dd(clause,cnf)) -> guess#(cnf) -->_1 guess#(dd(clause,cnf)) -> guess#(cnf):5 -->_1 guess#(dd(clause,cnf)) -> choice#(clause):4 6:W:member#(x,dd(y,ys)) -> eq#(x,y) -->_1 eq#(O(x),O(y)) -> c_6(eq#(x,y)):2 -->_1 eq#(#1(x),#1(y)) -> c_3(eq#(x,y)):1 7:W:member#(x,dd(y,ys)) -> member#(x,ys) -->_1 member#(x,dd(y,ys)) -> member#(x,ys):7 -->_1 member#(x,dd(y,ys)) -> eq#(x,y):6 8:W:sat#(cnf) -> guess#(cnf) -->_1 guess#(dd(clause,cnf)) -> guess#(cnf):5 -->_1 guess#(dd(clause,cnf)) -> choice#(clause):4 9:W:sat#(cnf) -> satck#(cnf,guess(cnf)) -->_1 satck#(cnf,assign) -> verify#(assign):10 10:W:satck#(cnf,assign) -> verify#(assign) -->_1 verify#(dd(l,ls)) -> verify#(ls):12 -->_1 verify#(dd(l,ls)) -> member#(negate(l),ls):11 11:W:verify#(dd(l,ls)) -> member#(negate(l),ls) -->_1 member#(x,dd(y,ys)) -> member#(x,ys):7 -->_1 member#(x,dd(y,ys)) -> eq#(x,y):6 12:W:verify#(dd(l,ls)) -> verify#(ls) -->_1 verify#(dd(l,ls)) -> verify#(ls):12 -->_1 verify#(dd(l,ls)) -> member#(negate(l),ls):11 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 8: sat#(cnf) -> guess#(cnf) 5: guess#(dd(clause,cnf)) -> guess#(cnf) 4: guess#(dd(clause,cnf)) -> choice#(clause) 3: choice#(dd(x,xs)) -> choice#(xs) *** Step 6.b:1.b:2: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: eq#(#1(x),#1(y)) -> c_3(eq#(x,y)) eq#(O(x),O(y)) -> c_6(eq#(x,y)) - Weak DPs: member#(x,dd(y,ys)) -> eq#(x,y) member#(x,dd(y,ys)) -> member#(x,ys) sat#(cnf) -> satck#(cnf,guess(cnf)) satck#(cnf,assign) -> verify#(assign) verify#(dd(l,ls)) -> member#(negate(l),ls) verify#(dd(l,ls)) -> verify#(ls) - Weak TRS: choice(dd(x,xs)) -> x choice(dd(x,xs)) -> choice(xs) guess(dd(clause,cnf)) -> dd(choice(clause),guess(cnf)) guess(nil()) -> nil() negate(#0(x)) -> #1(x) negate(#1(x)) -> #0(x) - Signature: {choice/1,eq/2,guess/1,if/3,member/2,negate/1,sat/1,satck/2,verify/1,choice#/1,eq#/2,guess#/1,if#/3 ,member#/2,negate#/1,sat#/1,satck#/2,verify#/1} / {#0/1,#1/1,O/1,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0 ,c_2/1,c_3/1,c_4/0,c_5/0,c_6/1,c_7/0,c_8/2,c_9/0,c_10/0,c_11/0,c_12/2,c_13/0,c_14/0,c_15/0,c_16/2,c_17/1 ,c_18/2,c_19/0} - Obligation: innermost runtime complexity wrt. defined symbols {choice#,eq#,guess#,if#,member#,negate#,sat#,satck# ,verify#} and constructors {#0,#1,O,dd,false,nil,true,unsat} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- #0 :: ["A"(9)] -(9)-> "A"(9) #1 :: ["A"(9)] -(9)-> "A"(9) #1 :: ["A"(5)] -(5)-> "A"(5) O :: ["A"(9)] -(0)-> "A"(9) O :: ["A"(5)] -(0)-> "A"(5) choice :: ["A"(9)] -(0)-> "A"(9) dd :: ["A"(9) x "A"(9)] -(9)-> "A"(9) dd :: ["A"(5) x "A"(5)] -(5)-> "A"(5) guess :: ["A"(9)] -(1)-> "A"(9) negate :: ["A"(9)] -(15)-> "A"(9) nil :: [] -(0)-> "A"(9) eq# :: ["A"(9) x "A"(5)] -(0)-> "A"(0) member# :: ["A"(9) x "A"(5)] -(1)-> "A"(0) sat# :: ["A"(11)] -(15)-> "A"(0) satck# :: ["A"(0) x "A"(9)] -(7)-> "A"(0) verify# :: ["A"(9)] -(7)-> "A"(0) c_3 :: ["A"(0)] -(0)-> "A"(6) c_6 :: ["A"(0)] -(0)-> "A"(14) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "#0_A" :: ["A"(1)] -(1)-> "A"(1) "#1_A" :: ["A"(1)] -(1)-> "A"(1) "O_A" :: ["A"(1)] -(0)-> "A"(1) "c_3_A" :: ["A"(0)] -(0)-> "A"(1) "c_6_A" :: ["A"(0)] -(0)-> "A"(1) "dd_A" :: ["A"(1) x "A"(1)] -(1)-> "A"(1) "nil_A" :: [] -(0)-> "A"(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: eq#(#1(x),#1(y)) -> c_3(eq#(x,y)) 2. Weak: eq#(O(x),O(y)) -> c_6(eq#(x,y)) *** Step 6.b:1.b:3: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: eq#(O(x),O(y)) -> c_6(eq#(x,y)) - Weak DPs: eq#(#1(x),#1(y)) -> c_3(eq#(x,y)) member#(x,dd(y,ys)) -> eq#(x,y) member#(x,dd(y,ys)) -> member#(x,ys) sat#(cnf) -> satck#(cnf,guess(cnf)) satck#(cnf,assign) -> verify#(assign) verify#(dd(l,ls)) -> member#(negate(l),ls) verify#(dd(l,ls)) -> verify#(ls) - Weak TRS: choice(dd(x,xs)) -> x choice(dd(x,xs)) -> choice(xs) guess(dd(clause,cnf)) -> dd(choice(clause),guess(cnf)) guess(nil()) -> nil() negate(#0(x)) -> #1(x) negate(#1(x)) -> #0(x) - Signature: {choice/1,eq/2,guess/1,if/3,member/2,negate/1,sat/1,satck/2,verify/1,choice#/1,eq#/2,guess#/1,if#/3 ,member#/2,negate#/1,sat#/1,satck#/2,verify#/1} / {#0/1,#1/1,O/1,dd/2,false/0,nil/0,true/0,unsat/0,c_1/0 ,c_2/1,c_3/1,c_4/0,c_5/0,c_6/1,c_7/0,c_8/2,c_9/0,c_10/0,c_11/0,c_12/2,c_13/0,c_14/0,c_15/0,c_16/2,c_17/1 ,c_18/2,c_19/0} - Obligation: innermost runtime complexity wrt. defined symbols {choice#,eq#,guess#,if#,member#,negate#,sat#,satck# ,verify#} and constructors {#0,#1,O,dd,false,nil,true,unsat} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- #0 :: ["A"(12)] -(12)-> "A"(12) #1 :: ["A"(12)] -(12)-> "A"(12) #1 :: ["A"(8)] -(8)-> "A"(8) #1 :: ["A"(10)] -(10)-> "A"(10) O :: ["A"(8)] -(8)-> "A"(8) choice :: ["A"(14)] -(0)-> "A"(14) dd :: ["A"(14) x "A"(14)] -(14)-> "A"(14) dd :: ["A"(8) x "A"(8)] -(8)-> "A"(8) dd :: ["A"(12) x "A"(12)] -(12)-> "A"(12) guess :: ["A"(14)] -(0)-> "A"(12) negate :: ["A"(12)] -(2)-> "A"(10) nil :: [] -(0)-> "A"(14) eq# :: ["A"(8) x "A"(8)] -(2)-> "A"(0) member# :: ["A"(10) x "A"(8)] -(1)-> "A"(0) sat# :: ["A"(15)] -(15)-> "A"(0) satck# :: ["A"(0) x "A"(12)] -(12)-> "A"(0) verify# :: ["A"(12)] -(9)-> "A"(0) c_3 :: ["A"(0)] -(0)-> "A"(4) c_6 :: ["A"(0)] -(0)-> "A"(14) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "#0_A" :: ["A"(1)] -(1)-> "A"(1) "#1_A" :: ["A"(1)] -(1)-> "A"(1) "O_A" :: ["A"(1)] -(1)-> "A"(1) "c_3_A" :: ["A"(0)] -(0)-> "A"(1) "c_6_A" :: ["A"(0)] -(0)-> "A"(1) "dd_A" :: ["A"(1) x "A"(1)] -(1)-> "A"(1) "nil_A" :: [] -(0)-> "A"(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: eq#(O(x),O(y)) -> c_6(eq#(x,y)) 2. Weak: WORST_CASE(?,O(n^3))